state\_after($e$;${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$2of(when{-}after($e$;${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$))